(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


 (** ** Real MMatrix Module *)
Require Import Reals.
Open Scope R_scope.
Require Export Matrix.MMat.MMatrix_Module.
Require Export Matrix.Mat.FMatrix.

Module FMMatrix := MMatrix FM.

Definition FMMO := FMMatrix.MMO.

Definition FMMI := FMMatrix.MMI.

Definition FMMeq := @FMMatrix.MMeq.
Arguments FMMeq {m}{n}{m2}{n2}.

Definition FMMadd := @FMMatrix.MMadd.
Arguments FMMadd {m0}{n0}{m}{n}.

Definition FMMopp := @FMMatrix.MMopp.
Arguments FMMopp {m0}{n0}{m}{n}.

Definition FMMsub := @FMMatrix.MMsub.
Arguments FMMsub {m0}{n0}{m}{n}.

Definition FMMmult := @FMMatrix.MMmult.
Arguments FMMmult {m}{n}{p}{m2} {n2} {p2}.

Definition FMMadd_comm:=@FMMatrix.MMadd_comm.
Definition FMMadd_assoc:=@FMMatrix.MMadd_assoc.
Definition FMMadd_zero_l:=@FMMatrix.MMadd_zero_l.
Definition FMMadd_zero_r:=@FMMatrix.MMadd_zero_r.

Definition FMMsub_opp:=@FMMatrix.MMsub_opp.
Definition FMMsub_assoc:=@FMMatrix.MMsub_assoc.
Definition FMMsub_zero_l:=@FMMatrix.MMsub_zero_l.
Definition FMMsub_zero_r:=@FMMatrix.MMsub_zero_r.
Definition FMMsub_self:=@FMMatrix.MMsub_self.

Definition FMMmul_add_distr_l:= @FMMatrix.MMmul_add_distr_l.
Definition FMMmul_add_distr_r:= @FMMatrix.MMmul_add_distr_r.
Definition FMMmul_sub_distr_l:= @FMMatrix.MMmul_sub_distr_l.
Definition FMMmul_sub_distr_r:= @FMMatrix.MMmul_sub_distr_r.
Definition FMMmul_assoc:= @FMMatrix.MMmul_assoc.
Definition FMMmul_zero_l := @FMMatrix.MMmul_zero_l.
Definition FMMmul_zero_r := @FMMatrix.MMmul_zero_r.

Definition FMMtteq:= @FMMatrix.MMtteq.
Definition FMMtrans_add:= @FMMatrix.MMtrans_add.
Definition FMMtrans_sub:= @FMMatrix.MMtrans_sub.
Definition FMMtrans_mul:= @FMMatrix.MMtrans_mul.




